es:event_system{i:l}, L:(Id List), e:es-E(es).
fischer{x:ut2, try:ut2, taken:ut2, contending:ut2, free:ut2, mine:ut2, wanted:ut2, z:ut2}
fischer(es; L)
 f-newround{x:ut2, free:ut2, mine:ut2}
 f-newround(es; L; e)
 (m:es-E(es)
 ((f-event{x:ut2}
 ((f-event(es; L; m)
 ( (f-rank{i:l}
 ( (f-rank(mkid{x:ut2}; mkid{free:ut2}; es; e)
 ( (=
 ( (inc-fst(f-rank{i:l}(mkid{x:ut2}; mkid{free:ut2}; es; m))
 ( ( (:  ))
 ( es-locl(es; m; e)
 ( @m(mkid{x:ut2}mkid{mine:ut2})
 ( e''[m,e).es-after(es; mkid{x:ut2}; e'') = mkid{mine:ut2}  Id)) 

latex

Definitions

True, T, ff, tt, let x = a in b(x), if b then t else f fi , Y, f-rank{i:l}(x; free; es; e), f-event{$x:ut2}(es; L; e), guard(T), sq_type(T), x. t(x), A c B, P  Q, x:A. B(x), es-locl(es; e; e'), es-dtype(es; i; x; T), prop{i:l}, t  T, A, mkid{$x:ut2}, P  Q, Id, x:A. B(x), Unit, , x(s), P  Q, False, @e(xv), f-newround{$x:ut2, $free:ut2, $mine:ut2}(es; L; e), fischer,

Lemmas

squash wf, not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, assert-eq-id, iff transitivity, eq id wf, eqtt to assert, bool wf, changed wf, es-when wf, loc-last-change, change-to-last-change, es-locl-iff, es-loc-pred, Id sq, es-after wf, alle-between1 wf, es-causl wf, inc-fst wf, f-rank wf, f-event wf, es-vartype wf, es-isconst wf, assert wf, last-change wf, event system wf, Id wf, es-E wf, fischer wf, f-newround wf, last-change-property, last-change-after-property, es-loc wf, es-dtype wf, id-deq wf, init-changed